\section{Method and class-level specifications}
We wrote method specifications that require the game to be in a particular state if a method can be called.
For example the method move requires the following: \textit{$(status == NOT\_STARTED || status == READY\_FOR\_MOVE)$}.

See Figure \ref{fig:statemachine} for an illustration of a state machine. This state machine shows all valid transitions.

\begin{center}
	\includegraphics[scale=.5]{StateMachineDiagram1.png}
	\captionof{figure}{State Machine}
	\label{fig:statemachine}
\end{center}

Furhermore the Table (\ref{tab:methodcalls}) shows possible method calls.
Note that only method calls are shown that make a transition which is not a self loop.
Also, we use \textbackslash result result as a condition which means that the transition depends on the result of the method call.

\begin{center}
	\begin{tabular}{llll}
		method         & condition                & State from               & State to              \\ \hline
		GameBoard()    & -                        & uninitialized            & not\_started          \\
		move()         & busy                     & not\_started             & busy\_updating        \\
		move()         & busy                     & ready\_for\_move         & busy\_updating        \\
		move()         & !busy                    & not\_started             & checking\_for\_winner \\
		move()         & !busy                    & ready\_for\_move         & checking\_for\_winner \\
		gameOver()     & !\textbackslash result   & checking\_for\_winner    & ready\_for\_move      \\
		gameOver()     & \textbackslash result    & not\_started             & finished              \\
		gameOver()     & \textbackslash result    & ready\_for\_move         & finished              \\
		gameOver()     & \textbackslash result    & checking\_for\_winner    & finished              \\
		update()       & busy                     & busy\_updating           & busy\_updating        \\
		update()       & !busy                    & busy\_updating           & checking\_for\_winner \\
		clearboard()   & -                        & uninitialized            & not\_started          \\
		clearboard()   & -                        & not\_started             & not\_started          \\
		clearboard()   & -                        & checking\_for\_winner    & not\_started          \\
		clearboard()   & -                        & ready\_for\_move         & not\_started          \\
		clearboard()   & -                        & finished                 & not\_started          \\
	\end{tabular}
	\captionof{table}{Possible method calls}
	\label{tab:methodcalls}
\end{center}

The following constructor and methods make self-loops as transitions in only the following states. Note that some methods are private and are thus not called in some states.

\begin{itemize}
\item \textit{dropping()} in all states except uninitialized.
\item \textit{check\_row()} in all states except uninitialized.
\item \textit{winnerOfColumn()} in all states except uninitialized.
\item \textit{gameOver()} in not\_started, ready\_for\_move and finished if !\textbackslash result.
\item \textit{field()} in all states except uninitialized.
\item \textit{notDone()} in all states except uninitialized.
\item \textit{empty\_below()} in all states except uninitialized.
\item \textit{status()} in all states except uninitialized and busy\_updating.
\item \textit{swap()} in busy\_updating
\item \textit{zero()} in busy\_updating
\item \textit{clear()} in all states
\item \textit{clearcolumn()} in all states
\end{itemize}

\section{Model variables}

We have defined the following model variables:

\begin{itemize}
\item \textit{board\_empty} every square on the board is \textit{Empty}.
\item \textit{board\_full} every square on the board is either a \textit{Cross} or a \textit{Circle}.
\item \textit{board\_of\_won\_game} there exists a vertical column, a horizontal column or a diagonal of length goal with all of them \textit{Circle}s or \textit{Cross}es.
\item \textit{board\_of\_game\_in\_progress} is expressed in !\textit{board\_of\_won\_game} \&\& !\textit{board\_full}.
\item \textit{game\_reset\_and\_board\_empty} the board is empty and gravity is turned off and it is Cross' turn and count is zero and winner is \textit{Empty} and busy is false.
\item \textit{board\_has\_valid\_dimensions} the board as an amount of rows equal to width and an amount of columns equal to height.
\end{itemize}

Table \ref{tab:methodcontracts} shows when the model variables are required or ensured.

\begin{center}
	\begin{tabular}{lll}
		Method   & precondition & postcondition \\ \hline
		clearboard() & - & game\_reset\_and\_board\_empty \\
		move() & board\_of\_game\_in\_progress & board\_of\_game\_in\_progress || board\_full || board\_of\_won\_game \\
	\end{tabular}
	\captionof{table}{Possible method calls}
	\label{tab:methodcalls}
\end{center}

For some loopinvariants we used board\_has\_valid\_dimensions. This suppressed warnings like nullpointers.
Initially, or after GameBoard is constructed by the constructor game\_reset\_and\_board\_empty must hold, so this is specified with the initially-clause.
In addition to the described contract so far we added more pre- and postconditions in order to suppress all warnings.

\section{Mistakes And Code Improvements}
We found the following mistakes:

\begin{enumerate}
\item \textit{check\_row()} contains a mistake where $(i + l)$ is multiplied by $di$ this can result in an index of zero when $di$ is zero. We improved this piece of code by replacing $(i+l)*di$ by $i+l*di$.
\item \textit{check\_row()} does not check if $i+l*di$ or $j+l*dj$ results in a negative number. This is not fatal so we did not improve the code on this, but we added a precondition, namely $0 <= di \&\& di <= 1 \&\& -1 <= dj \&\& dj <= 1$. This mistake is not fatal, because GameUI never executes the program in a sequence such that this behavior is triggered.
\item \textit{gameOver()} does not set a winner if the board is full. If a board is full the game can still have a winner. We rewrote gameOver() such that gameOver() first checks for a winner and then for a full board.
\item \textit{update()} contains a mistake in the while-loop. $bottom>=0$ should be evaluated before $board[x][bottom] != Empty$. We corrected this by switching both expressions.
\end{enumerate}

The mistakes can be found with the runtime checker when the following testcases are executed.

\subsection{Execution of mistake 1}
\begin{lstlisting}
gameBoard = new GameBoard(2,2,2);
assert(gameBoard.gameOver());
\end{lstlisting}

\subsection{Execution of mistake 2}
A testcase for mistake 2 can not be written.

\subsection{Execution of mistake 3}
\begin{lstlisting}
gameBoard = new GameBoard(3,3,3);
gameBoard.move(0,0);
gameBoard.gameOver();
gameBoard.move(0,1);
gameBoard.gameOver();
gameBoard.move(0,2);
gameBoard.gameOver();
gameBoard.move(1,0);
gameBoard.gameOver();
gameBoard.move(1,1);
gameBoard.gameOver();
gameBoard.move(1,2);
gameBoard.gameOver();
gameBoard.move(2,1);
gameBoard.gameOver();
gameBoard.move(2,0);
gameBoard.gameOver();
gameBoard.move(2,2);
gameBoard.gameOver();
assert(gameBoard.status().equals("won by X"));
\end{lstlisting}

\subsection{Execution of mistake 4}
\begin{lstlisting}
gameBoard = new GameBoard(3,3,3);
gameBoard.setGravity(true);
gameBoard.move(0,0);
gameBoard.update();
\end{lstlisting}

Furthermore we altered GameBoard.java to be able to suppress false positives from ESC/Java. For some reason ESC/Java has trouble dealing with loop invariants that contain nested forall's or that describe multi-dimensional arrays. Thus, we had to rewrite the methods \textit{update} and \textit{clearboard}. To this end, we added the three methods \textit{swapColumn}, \textit{swap} and \textit{zero} that are used by \textit{update}. For \textit{clearboard} we added two additional methods called \textit{clear} and \textit{clearcolumn}. We have added JavaDoc to explain non trivial specifications. The JavaDoc can be found in GameBoard.java.
